ma-frame-compat(A;B)
== adom(1of(2of(2of(2of(A))))). p=1of(2of(2of(2of(A))))(a)   B.rframe(A.pre p for a)
== & kxdom(1of(2of(2of(2of(2of(A)))))). 

== ef=1of(2of(2of(2of(2of(A)))))(kx)  
== efB.frame(1of(kx) affects 2of(kx))
== & B.aframe(1of(kx) affects 2of(kx))
== & B.rframe(A.effect ef of 1of(kx) on 2of(kx))
== & kldom(1of(2of(2of(2of(2of(2of(A))))))). 

== & snd=1of(2of(2of(2of(2of(2of(A))))))(kl)  
== & snd(tg:Id. (tg  map(p.1of(p);snd))  B.sframe(1of(kl) sends <2of(kl),tg>))
== & & B.bframe(1of(kl) sends on 2of(kl))
== & & B.rframe(A.sends snd of 1of(kl) on 2of(kl)) 

latex

---

clarification:

ma-frame-compat(A;B)
== fpf-all(Id; IdDeq; 1of(2of(2of(2of(A)))); a,p.B.rframe(A.pre p for a))
== & fpf-all((KndId);
== & fpf-all(product-deq(Knd;Id;KindDeq;IdDeq);
== & fpf-all(1of(2of(2of(2of(2of(A)))));
== & fpf-all(kx,ef.(B.frame(1of(kx) affects 2of(kx))
== & fpf-all(& B.aframe(1of(kx) affects 2of(kx))
== & fpf-all(& B.rframe(A.effect ef of 1of(kx) on 2of(kx))))
== & fpf-all((KndIdLnk);
== & fpf-all(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== & fpf-all(1of(2of(2of(2of(2of(2of(A))))));
== & fpf-all(kl,snd.((tg:Id.
== & fpf-all(kl,snd.(((tg  map(p.1of(p);snd)  Id)  B.sframe(1of(kl) sends <2of(kl),tg>))
== & fpf-all(& B.bframe(1of(kl) sends on 2of(kl))
== & fpf-all(& B.rframe(A.sends snd of 1of(kl) on 2of(kl)))) 

latex

Definitions	M.rframe(A.pre p for a), IdDeq, M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), xdom(f). v=f(x)   P(x;v), x:AB(x), product-deq(A;B;a;b), Knd, IdLnk, KindDeq, IdLnkDeq, P & Q, x:A. B(x), P  Q, (x  l), map(f;as), x.A(x), Id, M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), 1of(t), 2of(t)
FDL editor aliases	ma-frame-compat